\begin{tabbing}
$\forall$\=${\it es}$:ES, $T$:Type, ${\it eq}$:EqDecider($T$), $v$:$T$, $x$:Id, $e$:\{$e$:E$\mid$ @loc($e$)($x$:$T$)\} ,\+
\\[0ex]${\it e'}$:\{${\it e'}$:E$\mid$ $e$ $\leq$loc ${\it e'}$  \& ($x$ after ${\it e'}$) = $v$\} .
\-\\[0ex]$e$ $\leq$loc next event in [$e$;${\it e'}$] after which $x$ = $v$ 
\\[0ex]\& ($x$ after next event in [$e$;${\it e'}$] after which $x$ = $v$) = $v$
\\[0ex]\& $\forall$${\it e''}$$\in$[$e$,next event in [$e$;${\it e'}$] after which $x$ = $v$).$\neg$(($x$ after ${\it e''}$) = $v$)
\end{tabbing}